home *** CD-ROM | disk | FTP | other *** search
- Boolean : Type is
- const
- TRUE : Boolean
- FALSE : Boolean
- ops
- not : nil -> Boolean
- or : Boolean -> Boolean
- and : Boolean -> Boolean
- implies : Boolean -> Boolean
- iseq : Boolean -> Boolean # equivalence
- eqn
- # idempotence of not
- 'not( 'not(x)) = x
- 'not( TRUE) = FALSE
- # associativity of or
- x.or( y.or( z)) = (x.or(y)).or(z)
- # commutativity of or
- x.or( y) = y.or( x)
- x.or( TRUE) = TRUE
- x.or( FALSE) = x
- # definition of and
- 'and( x, y) = (x.not.or( y.not )).not
- # implication
- x.implies( y) = x.not.or( y)
- x.iseq( y) = x.implies( y).and( y.implies( x))
-
-